COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	final.f86[f86,jmc]	Fall 1986 cs306 final
C00004 00003	1. (15 points) gmat[x,y]  is true if the S-expression  x  is a
C00005 00004	2. (15 points) checksub[x,y,z,w] is true provided  w  is a correct result
C00006 00005	3. (10 points) size1 x  is the size of the list structure  x.  Take
C00007 00006	4. (25 points) size2 x is the size of a list structure computed
C00008 00007	5. (25 points) I received the following note from Gian-Luigi Bellin for
C00010 00008	6. (10 points) What does EKL have that the Boyer-Moore prover doesn't
C00011 ENDMK
C⊗;
final.f86[f86,jmc]	Fall 1986 cs306 final
CS306     FINAL EXAMINATION                           FALL 1986

	This take home examination is open book and notes.
Write LISP functions as follows except where something else is
requested.  Either notation may be used.  No collaboration.
Due noon Wednesday, December 17 in room 358 MJH.

1. (15 points) gmat[x,y]  is true if the S-expression  x  is a
``generalized match'' of the S-expression  y.  We require that
a CAR link in  x  corresponds to a CAR-CDR chain in  y  beginning
with CAR.  Likewise, a CDR link in  x  corresponds to a CAR-CDR
chain beginning with CDR.
  Thus  gmat[(A.B),((A.C).(B.B))]  is true.  (Actually
in two ways, since either  B  in  (B.B)  will serve).  As a second
example, we have  gmat[((A.B).C),((((D.A).B).D).(E.C))].
2. (15 points) checksub[x,y,z,w] is true provided  w  is a correct result
of substituting  x  for the atom  y  in  z.  All the arguments may be
assumed to be LISP function fragments, e.g. ((LAMBDA (X) (CONS X Y)) (CAR X))
  However,  x  and  z  may
contain lambda expressions, and meaning must be preserved.  Therefore,
substitutions are not legitimate that capture free variables.  The simplest
example where  checksub[x,y,z,w]  is not the same as  subst[x,y,z] = w  is
given by checksub[X,Y,(LAMBDA (X) (CONS X Y)),(LAMBDA (X) (CONS X X))].
3. (10 points) size1 x  is the size of the list structure  x.  Take
into account merging and possible circularity.
4. (25 points) size2 x is the size of a list structure computed
without backtracking, i.e. non-recursively.  You may assume that
the list structure word has two extra one bit parts.  These
parts are read by the functions  cpr x  and  ctr x  and changed
by the "functions"  rplacp[x,y]  and  rplact[x,y],  or if you
prefer Common Lisp's  SETF notation, they are changed by statements
of the form  (SETF (CPR X) Y)  and  (SETF (CTR X) Y).
5. (25 points) I received the following note from Gian-Luigi Bellin for
which I am grateful.

``∂08-Dec-86  0115	GLB  
Thank you. In case you wanted to have an EKL question in the final,
the following is a possibility:

;∀U.MEMBER(X,U)⊃NTH(U,FSTPOSITION(U,X))=X

;∀U N.UNIQUENESS(U)∧N<LENGTH U ⊃ FSTPOSITION(U,NTH(U,N))=N

It is easy, but not trivial.''

Prove the above propositions, where the definitions of the functions
are given in his report that was distributed.  You can either do
it informally or using EKL.  If you don't use EKL, be sure and
identify the statements on which induction is being done.

If you do it in EKL, the graders will be grateful and can hardly
avoid giving full credit if you get all the way through it.
6. (10 points) What does EKL have that the Boyer-Moore prover doesn't
and conversely?  Brief answers are preferred.  What problems do you
see in combining their virtues?